i:Id, l:IdLnk, tg, n, f, k:Top.
msg-spec-loc(k sends on l with tag tg [s,v.f(s,v)], at marker n;i)  (source(l) = i) 

latex

Definitions	t  T, x:A. B(x), source(l), Id, s = t, IdLnk, , type List, [], [car / cdr], (x  l), x:AB(x), P  Q, x.A(x), P  Q, x:A  B(x), P & Q, P  Q, {T}, x. t(x), Void, x:A.B(x), Top, x,y. t(x;y), msg-spec-loc(snd;i), SQType(T), s ~ t
Lemmas	IdLnk sq, top wf, msg-spec-links-spec1, iff functionality wrt iff, all functionality wrt iff, implies functionality wrt iff, member singleton, l member wf, IdLnk wf, Id wf, lsrc wf